Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add test to close #3666, problems with typechecking GADTs #4069

Closed
wants to merge 3 commits into from

Conversation

Blaisorblade
Copy link
Contributor

@Blaisorblade Blaisorblade commented Mar 4, 2018

Currently fails some checks in local testing and on CI, to investigate.

@Blaisorblade Blaisorblade changed the title Add test to close #3666 Add test to close #3666, problems with typechecking GADTs Mar 5, 2018
@Blaisorblade
Copy link
Contributor Author

Blaisorblade commented Mar 6, 2018

Log has a bunch of failures on tests/pos/i3666.scala:

assertion failure for Any <:< _, frozen = true
assertion failure for Any <:< T, frozen = true
...

@smarter
Copy link
Member

smarter commented Mar 6, 2018

The issue can be reduced to something like:

sealed trait Exp[T]                                                                                                                                                                                                                          
case class Var[T](name: String) extends Exp[T]                                                                                                                                                                                               
                                                                                                                                                                                                                                             
object Test {                                                                                                                                                                                                                                
  def env[T](x: Var[T]): T = ???                                                                                                                                                                                                             
                                                                                                                                                                                                                                             
  def eval[S](e: Exp[S]) = e match {                                                                                                                                                                                                         
    case v: Var[foo] =>                                                                                                                                                                                                                      
      env(v)                                                                                                                                                                                                                                 
  }                                                                                                                                                                                                                                          
}

This crashes when run through -Yno-deep-subtypes because of a loop in subtype checking:

==> isSubType Any <:< foo
  ==> isSubType Any <:< S
   ==> isSubType Any <:< foo

The problem becomes apparent when we turn on the gadts printer:

narrow gadt bound of type foo:  from below to S TypeRef(NoPrefix,type S) false
narrow gadt bound of type S:  from below to foo TypeRef(NoPrefix,type foo) false

We end up with GADT constraints foo >:> S and S >:> foo but we don't have a mechanism to unify GADT constraints, so we end up with a loop in subtyping checks. We could add a special case to handle simple unifications like this but it seems like to be completely general we really need to reuse all of ConstraintHandling to deal with GADT constraints too.

@odersky
Copy link
Contributor

odersky commented Mar 15, 2018

Good analysis, @smarter!

@biboudis
Copy link
Contributor

biboudis commented Apr 10, 2018

Maybe this example with polymorphic recursion is also related:

object Test {
 
  class Foo[A]
  case class Bar[A, B](f: B => Foo[A]) extends Foo[A]

  def meth[A](consumer: A => Unit, s: Foo[A]): Unit = {
    s match {
      case bar: Bar[a, bt] => {
        meth[bt](((e: bt) => meth(consumer, new Foo[a])), new Foo[bt])
      }
    }
  }
}

Again detected with -Yno-deep-subtypes.

assertion failure for Any <:< a, frozen = true
assertion failure for Any <:< A, frozen = true
assertion failure for Any <:< a, frozen = true
...

@smarter WDYT? What would be a workaround in my case (without disabling -Yno-deep-subtypes of course 😛)

@odersky odersky closed this May 28, 2018
@Blaisorblade Blaisorblade deleted the test-3666 branch September 6, 2018 21:38
sjrd added a commit to dotty-staging/dotty that referenced this pull request Mar 2, 2022
This includes a forward-port of the upstream changes in

* scala-js/scala-js@887d957
  Require an explicit name in @jsglobal for 'apply' and setter names.
* scala-js/scala-js@354cfdf
  Allow @jsglobal without explicit names inside Scala objects.
* scala-js/scala-js@9fa6a83
  Fix scala#4069: Make @jsimport's second arg default to the annotatee's name.
@sjrd sjrd mentioned this pull request Mar 2, 2022
griggt pushed a commit to griggt/dotty that referenced this pull request Mar 17, 2022
This includes a forward-port of the upstream changes in

* scala-js/scala-js@887d957
  Require an explicit name in @jsglobal for 'apply' and setter names.
* scala-js/scala-js@354cfdf
  Allow @jsglobal without explicit names inside Scala objects.
* scala-js/scala-js@9fa6a83
  Fix scala#4069: Make @jsimport's second arg default to the annotatee's name.
griggt pushed a commit to griggt/dotty that referenced this pull request Mar 22, 2022
This includes a forward-port of the upstream changes in

* scala-js/scala-js@887d957
  Require an explicit name in @jsglobal for 'apply' and setter names.
* scala-js/scala-js@354cfdf
  Allow @jsglobal without explicit names inside Scala objects.
* scala-js/scala-js@9fa6a83
  Fix scala#4069: Make @jsimport's second arg default to the annotatee's name.
griggt pushed a commit to griggt/dotty that referenced this pull request Apr 4, 2022
This includes a forward-port of the upstream changes in

* scala-js/scala-js@887d957
  Require an explicit name in @jsglobal for 'apply' and setter names.
* scala-js/scala-js@354cfdf
  Allow @jsglobal without explicit names inside Scala objects.
* scala-js/scala-js@9fa6a83
  Fix scala#4069: Make @jsimport's second arg default to the annotatee's name.
griggt pushed a commit to griggt/dotty that referenced this pull request Apr 6, 2022
This includes a forward-port of the upstream changes in

* scala-js/scala-js@887d957
  Require an explicit name in @jsglobal for 'apply' and setter names.
* scala-js/scala-js@354cfdf
  Allow @jsglobal without explicit names inside Scala objects.
* scala-js/scala-js@9fa6a83
  Fix scala#4069: Make @jsimport's second arg default to the annotatee's name.
griggt pushed a commit to griggt/dotty that referenced this pull request Apr 7, 2022
This includes a forward-port of the upstream changes in

* scala-js/scala-js@887d957
  Require an explicit name in @jsglobal for 'apply' and setter names.
* scala-js/scala-js@354cfdf
  Allow @jsglobal without explicit names inside Scala objects.
* scala-js/scala-js@9fa6a83
  Fix scala#4069: Make @jsimport's second arg default to the annotatee's name.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants